%{
#include <scdl/parser/common.hpp>
#include <scdl/parser/internal.hpp>
#include <scdl/parser/core.hpp>
#include <scdl/parser/StringMap.hpp>
#include <scdl/parser/Symbol.hpp>

#include <iostream>
#include <string>
#include <map>
#include <cstdio>
#include <cstdlib>
using std::cout;
using std::cerr;
using namespace scdl;

#ifdef WIN32
#define strdup _strdup
#define snprintf _snprintf
#endif

void yyrestart(FILE *input_file);

int yylex(); 
int yyerror(const char *p) { cerr << "Error: " << p << "\n"; return 0; }

namespace scdl {
        StringMap symbolTable;
}

int sentenceType;

%}

%union {
        char sym;
        bool bval;
        float number;
        char *strval;
        scdl::Symbol *symbol;
};
%token <sym>    ASSUME DEFINE BIND INDUCTIVE RECORD
%token <sym>    PRODUCT ASSIGN STEP
%token <sym>    OP
%token <strval> IDENT PARAMETER STRING
%token <bval>   BOOL
%token <number> NUMBER

%type  <strval> bind_starter ind_starter record_starter
%type  <symbol> application list ind_list
%type  <symbol> expr_root expr decl type_decl value
%type  <symbol> bind_record
%type  <symbol> record_entries record_entry_list record_entry

%right   PRODUCT

%destructor     { free($$); } <strval>

%locations
%debug

%%

script: sentence script | sentence

sentence: starter decl '.'
        {
                sentenceType = 0;
        }
        | bind_starter type_decl ASSIGN IDENT bind_record '.'
        {
                Identifier *sym = new Identifier;
                sym->setName($1);
                sym->setPosition(curfilename, @1.first_line, @1.first_column);
                if (makeBinder(sym, $2, $4)) {
                        sym->setRecord(static_cast<Record *>($5));
                        addIdentifier(sym);
                } else
                        delete sym;
        }
        | ind_starter type_decl ASSIGN ind_list '.'
        {
                List *list = static_cast<List *>($4);
                makeInductive($1, $2, list);
                sentenceType = 0;
        }
        | record_starter type_decl ASSIGN record_entries bind_record '.'
        {
                Identifier *sym = new Identifier;
                sym->setName($1);
                sym->setPosition(curfilename, @1.first_line, @1.first_column);
                sym->setType($4->getType());
                sym->setDef($4);
                addIdentifier(sym);
                sentenceType = 0;
        }

starter: ASSUME
        {
                sentenceType = ASSUME;
        }
       | DEFINE
        {
                sentenceType = DEFINE;
        }

bind_starter: BIND IDENT
        {
                touchList($2);
                sentenceType = BIND;
                $$ = $2;
        }

ind_starter: INDUCTIVE IDENT
        {
                touchList($2);
                sentenceType = INDUCTIVE;
                $$ = $2;
        }

record_starter: RECORD IDENT
        {
                touchList($2);
                sentenceType = RECORD;
                $$ = $2;
        }

decl: IDENT type_decl value
        {
                Identifier *sym = new Identifier;
                sym->setName($1);
                sym->setPosition(curfilename, @1.first_line, @1.first_column);
                bool ret = false;
                switch(sentenceType) {
                case ASSUME:
                        ret = makeAssumption(sym, $2, $3); break;
                case DEFINE:
                        ret = makeDefinition(sym, $2, $3); break;
                }

                if (ret)
                        addIdentifier(sym);
                else
                        delete sym;
        }
    | decl ',' IDENT type_decl value
    {
                Identifier *sym = new Identifier;
                sym->setName($3);
                sym->setPosition(curfilename, @3.first_line, @3.first_column);
                bool ret = false;
                switch(sentenceType) {
                case ASSUME:
                        ret = makeAssumption(sym, $4, $5); break;
                case DEFINE:
                        ret = makeDefinition(sym, $4, $5); break;
                }

                if (ret)
                        addIdentifier(sym);
                else
                        delete sym;
        }

type_decl: ':' expr_root
        {
                $$ = $2;
        }
         | /* empty */
        {
                $$ = 0;
        }

value: ASSIGN expr_root
        {
                $$ = $2;
        }
     | /* empty */
        {
                $$ = 0;
        }

expr_root: STRING
        {
                String *sym = new String;
                sym->setPosition(curfilename, @1.first_line, @1.first_column);
                sym->setType(getIdentifier("String"));
                sym->setValue($1);
                $$ = sym;
        }
         | NUMBER
        {
                Number *sym = new Number;
                sym->setPosition(curfilename, @1.first_line, @1.first_column);
                sym->setType(getIdentifier("Number"));
                sym->setValue($1);
                $$ = sym;
        }
         | BOOL
        {
                Boolean *sym = new Boolean;
                sym->setPosition(curfilename, @1.first_line, @1.first_column);
                sym->setType(getIdentifier("Bool"));
                sym->setValue($1);
                $$ = sym;
        }
         | IDENT
        {
                Symbol *sym = 0;
                if (symbolTable.find($1)) {
                        sym = symbolTable[$1];
                        /* Definition inline if possible */
                        Identifier *id = getIdentifier($1);
                        if (id) {
                                if (id->getCategory() == CATEGORY_DEFINITION)
                                        sym = id->getDef();
                                else
                                        sym = id;
                        }
                } else if (sentenceType == INDUCTIVE) {
                        /* Only for passing the name.
                         * Should be deleted right after the inductive type is defined.
                         */
                        Identifier *id = new Identifier;
                        id->setPosition(curfilename, @1.first_line, @1.first_column);
                        id->setName($1);
                        sym = id;
                }

                $$ = sym;
        }
         | PARAMETER
        {
                Parameter *sym = new Parameter;
                sym->setPosition(curfilename, @1.first_line, @1.first_column);
                sym->setName($1);
                $$ = sym;
        }
         | expr_root PRODUCT expr_root
        {
                NamedSymbol *left = static_cast<NamedSymbol *>($1),
                            *right = static_cast<NamedSymbol *>($3);
                char buf[256];
                snprintf(buf, 256, "(%s)->(%s)", left->getName(), right->getName());
                Symbol *type = getType(buf);
                if (type) {
                        $$ = type;
                } else {
                        Product *sym = new Product;
                        sym->setPosition(curfilename, left->line(), left->column());
                        sym->setType(getIdentifier("Set"));
                        sym->setName(buf);
                        sym->setFactor(left, right);
                        symbolTable[buf] = sym;
                        $$ = sym;
                }
        }
         | '(' expr ')'
        {
                $$ = $2;
        }
         | '[' list ']'
        {
                $$ = $2;
        }

expr: expr_root
    | application
    | OP expr_root expr_root
        {
                $$ = calculateConstant($1, $2, $3);
                $$->setPosition(curfilename, @1.first_line, @1.first_column);
        }

application: expr_root expr_root
        {
                Application *sym = new Application;
                sym->setPosition(curfilename, @1.first_line, @1.first_column);
                sym->pushElement($1);
                sym->pushElement($2);
                resolveParameter(sym->getApplier(), $2);
                $$ = sym;
        }
           | application expr_root
        {
                Application *sym = static_cast<Application *>($1);
                sym->pushElement($2);
                resolveParameter(sym->getApplier(), $2);
                $$ = sym;
        }

list: expr_root
        {
                List *sym = new List;
                sym->setPosition(curfilename, @1.first_line, @1.first_column);
                if ($1->getType() != getIdentifier("ListSort")) {
                        /* Default to be a serial list. */
                        sym->pushElement(getIdentifier("Serial"));
                }
                sym->pushElement($1);
                $$ = sym;
        }
    | list expr_root
        {
                List *sym = static_cast<List *>($1);
                sym->pushElement($2);
                $$ = sym;
        }

ind_list: expr_root
        {
                List *sym = new List;
                sym->setPosition(curfilename, @1.first_line, @1.first_column);
                sym->pushElement($1);
                $1->unref();
                $$ = sym;
        }
        | ind_list '|' expr_root
        {
                List *sym = static_cast<List *>($1);
                sym->pushElement($3);
                $3->unref();
                $$ = sym;
        }

bind_record: record_entries
           | '{' RECORD IDENT '}'
        {
                Symbol *record = 0;
                Identifier *id = getIdentifier($3);
                if (id && id->getCategory() == CATEGORY_DEFINITION &&
                    id->getType() == getIdentifier("Struct"))
                        record = id->getDef();
                $$ = record;
        }
           | /* empty */
        {
                $$ = 0;
        }

record_entries: '{' record_entry_list '}'
        {
                $$ = $2;
        }

record_entry_list: record_entry
        {
                Record *sym = new Record;
                sym->setPosition(curfilename, @1.first_line, @1.first_column);
                sym->setType(getIdentifier("Struct"));
                sym->pushElement($1);
                $1->unref();
                $$ = sym;
        }
                 | record_entry_list ',' record_entry
        {
                Record *sym = static_cast<Record *>($1);
                sym->pushElement($3);
                $3->unref();
                $$ = sym;
        }

record_entry: IDENT ':' expr_root
        {
                Identifier *sym = new Identifier;
                sym->setName($1);
                sym->setPosition(curfilename, @1.first_line, @1.first_column);
                sym->setType($3);
                $$ = sym;
        }

%%

struct BuiltinTypes {
        const char *name;
        const char *type;
};

BuiltinTypes builtins[] = {
        {"Type", 0},
        {0, 0}
};

void add_builtin_types(StringMap &symTable)
{
        BuiltinTypes *builtin = builtins;
        while (builtin->name != 0) {
                Symbol *type = 0;
                if (builtin->type) {
                        type = getIdentifier(builtin->type);
                }
                Identifier *sym= new Identifier();
                sym->setPosition("<builtin>", 0, 0);
                sym->setName(builtin->name);
                sym->setType(type);
                if (!addIdentifier(sym))
                        delete sym;
                builtin ++;
        }
}

int scdl_parse(char *path)
{

        FILE *f = fopen(path, "r");
        if (!f)
                return -1;

        curfilename = path;
        symbolTable.clear();
        add_builtin_types(symbolTable);
        parse_builtin();
        symbolTable.clearPrintChain();

        yyrestart(f);
        yyparse();
        fclose(f);

        return 0;
}

scdl::StringMap *get_symbol_table()
{
        return &symbolTable;
}
